Library cross_difference

Require Export PointsType.
Require Import incidence.
Require Import isogonal_conjugate.

Open Scope R_scope.

Section Triangle.

Context `{M:triangle_theory}.

Definition cross_difference P U :=
 match P,U with
  cTriple p q r, cTriple u v w ⇒
  cTriple (q×w - r×v) (r×u - p×w) (p×v - q×u)
 end.

Lemma cross_difference_property :
  ∀ P U,
   match P,U with
     cTriple X Y Z, cTriple X2 Y2 Z2 ⇒
      X × Y2 - X2 × Y ≠ 0 →
      Y × Z2 - Y2 × Z ≠ 0 →
      Z × X2 - Z2 × X ≠ 0 →
   eq_points (cross_difference P U) (isogonal_conjugate (trilinear_pole (line P U)))
  end.
Proof.
intros.
destruct P.
destruct U.
unfold eq_points, trilinear_pole, cross_difference, isogonal_conjugate.
simpl.
split;
field;
repeat split;assumption.
Qed.

End Triangle.